\begin{nusmvCommand}{gen\_ltlspec\_bmc\_onepb}{Dumps into one dimacs file the problem generated for the given LTL specification, or for all LTL specifications if no formula is explicitly given. Generation and dumping parameters are the problem bound and the loopback value}

 \cmdLine{gen\_ltlspec\_bmc\_onepb [-h | -n idx | -p "formula" \linebreak[4][IN context]] [-k length] [-l loopback] [-o filename]}
 
As the \command{gen\_ltlspec\_bmc} command, but it generates and dumps
only one problem given its bound and loopback. 

\begin{cmdOpt}

\opt{-n \parameter{\natnum{\it index}}}{ {\it index} is the numeric index of a valid LTL
specification formula actually located in the properties database.
The validity of {\it index} value is checked out by the system.}

\opt{-p \parameter{"\anyexpr [IN context]"}}{ Checks the \anyexpr specified
on the command-line. \code{context} is the module instance name which
the variables in \anyexpr must be evaluated in.}

\opt{-k \parameter{\natnum{\it length}}}{ {\it length} is the single problem bound used
to generate and dump it. Only natural numbers are valid values for this
option.  If no value is given the environment variable \envvar{
bmc\_length} is considered instead.  }

\opt{-l \parameter{\set{\it loopback}{\range{0}{length-1},
       \range{-1}{-length}, X, * }}}{The {\it loopback} value may be: }
       \tabItem{a natural number in (0, {\it length-1}). A positive sign ('+') can 
       be also used as prefix of the number. Any invalid combination of length 
       and loopback will be skipped during the generation and dumping 
       process.}
       \tabItem{negative number in (-1, -{\it length}). 
       Any invalid combination of length and loopback will be skipped during 
       the generation process.}
       \tabItem{the symbol `\varvalue{X}', which means ``no loopback".}
       \tabItem{the symbol `\varvalue{*}', which means ``all possible loopback from zero to 
       {\it length-1}".}

\opt{-o \parameter{\filename{\it filename}}}{
 {\it filename} is the name of the dumped dimacs file. If this
       options is not specified, variable \varName{bmc\_dimacs\_filename} will be
       considered. The file name string may contain special symbols which 
       will be macro-expanded to form the real file name. 
       Possible symbols are: }
       \tabItem{ @F: model name with path part }
       \tabItem{ @f: model name without path part} 
       \tabItem{ @k: current problem bound} 
       \tabItem{ @l: current loopback value} 
       \tabItem{ @n: index of the currently processed formula in the property 
       database }
       \tabItem{ @@: the '@' character}

\end{cmdOpt}

\end{nusmvCommand}
